$\forall$${\it es}$:event\_system\{i:l\}, $e$,${\it e'}$:es{-}E(${\it es}$), $l$:IdLnk.
\\[0ex](${\it e'}$ $\in$ es{-}receives(${\it es}$; $e$; $l$))
\\[0ex]$\Leftarrow\!\Rightarrow$ (($\uparrow$es{-}isrcv(${\it es}$; ${\it e'}$)) c$\wedge$ ((es{-}sender(${\it es}$; ${\it e'}$) = $e$) $\wedge$ (es{-}lnk(${\it es}$; ${\it e'}$) = $l$)))